Isn't this rule the same as the rule two lines up, with x and y swapped? In general I like that we're doing commutativity explicitly here but I think that in this case it's actually just a redundant match -- we'll match the same patterns again with renamed bindings, so the effect is that we'll always add two iadds to the egraph (which is not what we want).

Same pattern in the rest of this rule's variants I believe.

I would have expected the overlap checker to find true redundancies, do you know why it isn't in this case?

These are in the mid-end so simplify is a multi-constructor (e-graphs!) -- we disable the overlap checker completely for this case.

I guess in theory a static check might still be possible but it would have to be something like: LHSes both fire and RHSes are exactly the same, which is much harder (need to see into external ctor semantics in the general case).

(The driver should dedup the same Value coming back twice though -- see here)

Thanks for pointing this out. I’ve fixed the duplicated rules.

I think the "redundancy" is somewhat confusing to me, and I think it'd better if we can clarify here.

The README says that commutative cases are better explicitly coded, not assumed by the compiler or overly generalized with other meta-rules. I see the redundant rules here are to exploit the commutativity, following the doc. Let me know if I'm missing something. Thanks!

@bongjunj I think the issue here is that the left-hand sides are not even different commutative variants but literally the same (just alpha-renamed, i.e. with different binding spellings). With the right-hand sides the same, the effect of this is that matching with a particular x and y will produce both (iadd x y) and (iadd y x) as terms (so I was wrong above: this won't actually dedup -- and there's no reason to have both those forms produced when we don't have further information about x and y).

Said another way: what the README is describing is that we should have all commutative variants as left-hand sides explicitly in variations of a rule. But what the rules are doing here is not moving around pieces on the left-hand side, but just matching the same thing (always exactly equivalently) with different names.

I think "don't write the same left-hand side twice" is probably already implied by our rules but I'm happy to review a PR if you think it could be made more explicit!

Ah, now I see what the rules are doing. Thanks for the detailed comment!!